\begin{tabbing}
lpath($p$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:\{0..($\parallel$$p$$\parallel-$1)$^{-}$\}.\+
\\[0ex]destination($p$[$i$]) $=$ source($p$[$i$+1]) $\in$ Id \& $\neg$$p$[$i$+1] $=$ lnk{-}inv($p$[$i$]) $\in$ IdLnk
\-
\end{tabbing}